Inference at * 2 
Iof proof for Lemma can-apply-fun-exp-add-iff:



1. A : Type
2. n : 
3. m : 
4. f : A(A + Top)
5. x : A
6. (can-apply(f^m;x)) & (can-apply(f^n;do-apply(f^m;x)))
  can-apply(f^n+m;x) 

latex

 by InteriorProof ((RWO "p-fun-exp-add" 0) 
CollapseTHENA (Auto)) 

latex

Co1: 

Co1:   can-apply(f^n o f^m  ;x)
Co.

Definitions	P  Q, , T, suptype(S; T), P  Q, P  Q, S  T, x:A.B(x), Void, x:A. B(x), Top, left + right, True, t  T, P & Q, x:A  B(x), n+m, can-apply(f;x), f o g  , f^n, b, x:AB(x), , s = t, , Type
Lemmas	iff wf, rev implies wf, assert wf, bool wf, can-apply wf, squash wf, true wf, p-fun-exp-add, member wf, top wf